/*************************************************************************
	> File Name: maxTomin.c
	> Author:
	> Mail:
	> Created Time: 2017年02月04日 星期六 14时07分14秒
 ************************************************************************/

#include<stdio.h>
#include <stdlib.h>
#include <string.h>
#include<klee/klee.h>
#include "klee_change_macros.h"
int main(int argc, char* argv[]){
    int a,b,d;
    a=atoi(argv[1]);
    b=atoi(argv[2]);
    char *aa=argv[1], *bb=argv[2];
//if(klee_change(a>b,a<4))
    if(argv[1]>argv[2])
    {
        char *as="old version", *bs="new version";
//        char * ss=(char*)klee_change(as,bs);
  //      char *ss=(char *)klee_change("old_version","new_version");
        char *ss=(char *)klee_change(a,b);
        printf("%s",ss);
    }
    else
        printf("%d",(int)klee_change(3,5));
 //   else
       // printf("%d",(int)klee_change(a,b));
    return 0;
}
